A De Morgan Heyting category is a Heyting category (such as a topos or pretopos) in which for every object the pseudocomplement of the intersection of two subobjects and is the union of the pseudocomplements of and , . Equivalently, it is a Heyting category in which for every object the union of the pseudocomplement of every subobject and the double pseudocomplement of is an improper subobject, , .
Therefore, the subobject poset of any object is a De Morgan Heyting algebra. De Morgan's law and weak excluded middle hold in the internal logic of .
In addition, every De Morgan Heyting category is a first order De Morgan Heyting hyperdoctrine given by the subobject poset functor .
Every De Morgan topos is a De Morgan Heyting category.
The category Set of sets and functions in strongly predicative constructive mathematics with weak excluded middle is a De Morgan Heyting category.
Last revised on November 16, 2022 at 20:58:16. See the history of this page for a list of all contributions to it.